es:ES, A, V:Type, i:Id, knd:Knd, ds:x:Id fp Type, f:(State(ds)V(A + Top)).
(e:E. (loc(e) = i)  (kind(e) = knd)  ((valtype(e) r V) & (state@loc(e) r State(ds))))
 (es-trigger(es;i;knd;ds;f)  AbsInterface(A)) 

latex

Definitions

t  T, P & Q, P  Q, x:A. B(x), t.1, E, s = t, val(e), x:A  B(x), b, ES, Type, Atom$n, Id, left + right, Knd, a:A fp B(a), x:AB(x), P  Q, P  Q, vartype(i;x), Top, f(x)?z, IdDeq, x.A(x), x. t(x), f(a), EState(T), , pred!(e;e'), SWellFounded(R(x;y)), loc(e), <a, b>, A, constant_function(f;A;B), kindcase(k; a.f(a); l,t.g(l;t) ), , e < e', r  s, val-axiom(E;V;M;info;pred?;init;Trans;Choose;Send;val;time), , Unit, Msg(M), type List, IdLnk, EOrderAxioms(E; pred?; info), EqDecider(T), let x,y = A in B(x;y), False, ff, if b then t else f fi , valtype(e), kind(e), {T}, SQType(T), s ~ t, case b of inl(x) => s(x) | inr(y) => t(y), State(ds), state@i, @i discrete ds, , (state when e), inr x , loc(e), a = b, a = b, p  q, es-trigger(es;i;knd;ds;f), AbsInterface(A)

Lemmas

all functionality wrt iff, implies functionality wrt iff, band wf, eq knd wf, es-kind wf, eq id wf, es-loc wf, ifthenelse wf, eqtt to assert, eqff to assert, iff transitivity, assert of bnot, not functionality wrt iff, assert-eq-id, bfalse wf, es-state-when wf, es-state-subtype2, es-state-subtype, subtype rel dep function, subtype rel self, Id sq, val-axiom wf, constant function wf, fpf-cap wf, Id wf, id-deq wf, es-state-subtype-iff, assert-eq-knd, es-val wf